COMMENT ⊗   VALID 00008 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	facts about nth, nthcdr and fstposition
C00004 00003	forms of doubleinduction
C00012 00004	basic facts about nth
C00022 00005	nthcdr
C00025 00006	fstposition
C00027 00007	injectivity 
C00028 00008	miscellaneous facts: nth, allp and mklset
C00037 ENDMK
C⊗;
;facts about nth, nthcdr and fstposition
(wipe-out)
(get-proofs length prf ekl sys)
 
(proof lispax)
;now we need to tie up natural numbers and s-expressions

(axiom |∀n.sexp n|)
(label simpinfo)

(axiom |∀n.¬null(n)|)
(label simpinfo)

(proof sets)
;all numbers will be urelements

(axiom |∀n.urelement n|)
(label simpinfo)

;forms of doubleinduction
(proof listinduction)

;a convenient form for double induction on lists

(axiom |∀phi2.(∀u v x y.phi2(nil,u)∧phi2(u,nil)∧(phi2(u,v)⊃phi2(x.u,y.v)))⊃(∀u v.phi2(u,v))|)
(label doubleinduction)

;the next principle gives a form of double induction for lists and numbers

(axiom |∀phi3.(∀u n x.phi3(nil,n)∧phi3(u,0)∧(phi3(u,n)⊃phi3(x.u,n')))⊃(∀u n.phi3(u,n))|)
(label doubleinduction1)

;basic facts about nth
(proof nth)

;1
(decl nth (syntype: constant) (type: |ground⊗ground→ground|))

;2
(defax  nth |∀x u n.nth(nil,n)=nil∧nth(u,0)=car u∧
                    nth(x.u,n')=nth(u,n)|)
(label simpinfo) (label nthdef)

;well-definedness of nth 

;3
(axiom |∀u n.sexp nth(u,n)|)
(label simpinfo)(label sexp_nth)

;membership of nth in the original list

;4
(axiom |∀u n.n<length u⊃member(nth(u,n),u)|)
(label nthmember)

;we need a converse of nthmember

;5
(axiom |∀u y.member(y,u)⊃(∃n.n<length u∧nth(u,n)=y)|)
(label member_nth)

;nthcdr
(proof nthcdr)

;1
(decl nthcdr (syntype: constant) (type: |ground⊗ground→ground|))

;2
(defax  nthcdr |∀x u n.nthcdr(nil,n)=nil∧nthcdr(u,0)=u∧
                              nthcdr(x.u,n')=nthcdr(u,n)|)
(label simpinfo) (label nthcdrdef)

;3
(axiom |∀u n.listp nthcdr(u,n)|)
(label simpinfo)

;4
;nth nthcdr zero

(axiom |∀u.0<length u⊃nth(u,0).nthcdr(u,1)=u|)
(label nth_nthcdr_zero)

;5
;car nthcdr

(axiom |∀u n.n<length u⊃car nthcdr(u,n)=nth(u,n)|)
(label car_nthcdr)

;6
;cdr nthcdr

(axiom |∀u n.cdr nthcdr(u,n)=nthcdr(u,n')|)
(label cdr_nthcdr)

;7
;nthcdr car cdr

(axiom |∀u n.n<length u⊃nthcdr(u,n)=nth(u,n).nthcdr(u,n')|)
(label nthcdr_car_cdr)

;8
;nth in nthcdr

(axiom |∀u n m.n≤m∧m<length u⊃member(nth(u,m),nthcdr(u,n))|)
(label nth_in_nthcdr)

;9
;nth nthcdr

(axiom |∀u n m.n<length u∧m<length (nthcdr(u,n))⊃nth(nthcdr(u,n),m)=nth(u,m+n)|)
(label nth_nthcdr)

;10
;length nthcdr

(axiom |∀u n.n≤length u⊃length (nthcdr(u,n))=length u-n|)
(label length_nthcdr)

;11
(axiom |∀u.nthcdr(u,length u)=nil|)
(label last_nthcdr)

;12
(axiom |∀u n.length(u)≤n⊃nthcdr(u,n)=nil|)
(label trivial_nthcdr)

;13
(axiom |∀a u n.allp(a,u)⊃allp(a,nthcdr(u,n))|)
(label allp_nthcdr)

;local listinduction, using nth and nthcdr

;14
(axiom |∀phi4 u.phi4(nil,length u)∧
 (∀n.n<length u∧phi4(nthcdr(u,n'),n')⊃phi4(nth(u,n).nthcdr(u,n'),n))⊃phi4(u,0)|)
(label nthcdr_induction1)

;15
(axiom |∀phi u.phi(nil)∧(∀n.n<length(u)⊃
               (phi(nthcdr(u,n'))⊃phi(nth(u,n).nthcdr(u,n'))))⊃phi(u)|)
(label nthcdr_induction)
;fstposition
(proof fstposition)

(decl (fstposition) (syntype: constant) (type: |ground⊗ground→ground|))
(define fstposition |∀x u y.fstposition(nil,y)=nil∧
                        fstposition(x.u,y)=if ¬member(y,x.u) then nil else
                                        if x=y then 0 else add1(fstposition(u,y))|
                                        listinductiondef)
(label fstpositiondef)

(axiom |∀u y.(null fstposition(u,y)⊃¬member(y,u))∧
             (member(y,u)⊃natnum(fstposition(u,y)))∧
             (null fstposition(u,y)∨natnum(fstposition(u,y)))|)
(label simpinfo)(label posfacts)

(axiom |∀u y.sexp fstposition(u,y)|)
(label simpinfo)(label sortpos)

(axiom |∀u y.member(y,u)⊃fstposition(u,y)<length u|)
(label pos_length)

(axiom |∀u n.member(n,u)⊃nth(u,fstposition(u,n))=n|)
(label nth_fstposition)

(axiom |∀u n.uniqueness(u)∧member(n,u)⊃fstposition(u,nth(u,n))=n|)
(label fstposition_nth)

;injectivity 
;another predicate for uniqueness

(proof inj)

(decl (inj) (syntype: constant) (type: |ground→truthval|))
(define inj |∀u.inj(u)=∀n m.n<length(u)∧m<length(u)∧nth(u,n)=nth(u,m)⊃n=m|)
(label injdef)

(axiom |∀u.uniqueness(u)≡inj(u)|)
(label uniqueness_injectivity)
;miscellaneous facts: nth, allp and mklset
(proof allp)

(axiom |∀phi1 u.(∀n.n<length u⊃phi1(nth(u,n)))⊃allp(phi1,u)|)
(label nth_allp)

(proof setfacts)
;fact about mkset and mklset

(axiom |∀u.mklset(u)=(λx.(∃k.k<length u∧nth(u,k)=x))|)
(label mklset_fact)

(save-proofs nth)